A polynomial time complete disjunction property in intuitionistic propositional logic

摘要

We extend the polynomial time algorithms due to Buss and Mints(APAL 1999) andFerrari, Fiorentini and Fiorino(LPAR 2002) to yield a polynomial time completedisjunction property in intuitionistic propositional logic.